M1, M2:MsgA. M1 || M2  M2  M1  M2 

latex

Definitions

P  Q, x:A. B(x), x. t(x), Knd, Type, f  g, Void, KindDeq, f  g, rcv(l,tg), Top, IdLnk, t.1, Id, IdDeq, f(x)?z, type List, t  T, x.A(x), State(ds), x:AB(x), x:A  B(x), t.2, , , a:A fp B(a), product-deq(A;B;a;b), IdLnkDeq, P & Q, A c B, Valtype(da;k), MsgA, M1 ||decl M2, mk-ma, M1  M2, M1  M2, M1 || M2

Lemmas

ma-compatible wf, msga wf, Id wf, id-deq wf, Knd wf, Kind-deq wf, IdLnk wf, idlnk-deq wf, fpf-trivial-subtype-top, product-deq wf, bool wf, rationals wf, pi1 wf, top wf, fpf-join wf, rcv wf, pi2 wf, fpf-sub-join-left, subtype-fpf2, ma-state wf, subtype rel product, subtype rel dep function, subtype rel self, subtype rel function, fpf-cap wf, subtype rel list, subtype-fpf-cap-top, subtype-fpf-cap-void, fpf-sub-join-right